
from chaotic_ex import chaotic_ex
from interval import State, bottom, top, assign, force_range, force_less, iota, Range, ScanfExp, AddConstExp, ConstExp, Inf, inf, force_exclude_from_range

succ = {
    0: set([1]),
    1: set([2]),
    2: set([3,31]),
    3: set([4,13,20,26]),
    4: set([5]),
    5: set([6,8]),
    6: set([7]),
    7: set([31]),
    8: set([9]),
    9: set([10]),
    10: set([11]),
    11: set([12]),
    12: set([30]),
    13: set([14]),
    14: set([15,17]),
    15: set([16]),
    16: set([31]),
    17: set([18]),
    18: set([19]),
    19: set([30]),  
    20: set([21]),
    21: set([22]),
    22: set([23,25]),
    23: set([24]),
    24: set([22]),
    25: set([30]),
    26: set([27]),
    27: set([28]),
    28: set([31]),
    29: set([30]),
    30: set([1]),
    31: set([]),
        } # CFG edges


EOF = 0xff
SIZE = 1000
nop = lambda state: state
tr = {
    (0, 1): lambda state: assign(state, 'top', ConstExp(0)),
    (1, 2): lambda state: assign(state, 'kind', ScanfExp()),
    (2, 3): lambda state: force_exclude_from_range(state, 'kind', EOF),
    (2, 31): lambda state: force_range(state, 'kind', Range(EOF,EOF)),
    (3, 4): lambda state: force_range(state, 'kind', Range(0,0)),
    (3, 13): lambda state: force_range(state, 'kind', Range(1,1)),
    (3, 20): lambda state: force_range(state, 'kind', Range(2,2)),
    (3, 26): lambda state: force_range(state, 'kind', Range(3,Inf)),
    (4, 5): nop,
    (5, 6): lambda state: force_range(state, 'top', Range(SIZE,Inf)),
    (5, 8): lambda state: force_range(state, 'top', Range(inf,SIZE-1)),
    (6, 7): nop,
    (7, 31): nop,
    (8, 9): nop,
    (9, 10): lambda state: assign(state, 'data', ScanfExp()),
    (10, 11): nop,#'stack[top] = data',
    (11, 12): lambda state: assign(state, 'top', AddConstExp('top', 1)),
    (12, 30): nop,
    (13, 14): nop,
    (14, 15): lambda state: force_range(state, 'top', Range(inf,0)),
    (14, 17): lambda state: force_range(state, 'top', Range(1,Inf)),
    (15, 16): nop,
    (16, 31): nop,
    (17, 18): lambda state: assign(state, 'top', AddConstExp('top', -1)),
    (18, 19): nop,#'printf("top of the stack is %d\n", stack[top])',
    (19, 30): nop,
    (20, 21): nop,
    (21, 22): lambda state: assign(state, 'i', ConstExp(0)),
    (22, 23): lambda state: force_less(state, 'i', 'top'), #'i < top',
    (22, 25): lambda state: force_less(state, 'top', 'i', True), #'i >= top',
    (23, 24): nop, #'printf("stack[%d]=%d\n", i, stack[i])',
    (24, 22): lambda state: assign(state, 'i', AddConstExp('i',1)),
    (25, 30): nop,
    (26, 27): nop,
    (27, 28): nop,
    (28, 31): nop,
    (29, 30): nop,
    (30, 1): nop,
    } # transfer function

tr_txt  = {
    (0, 1): "top = 0 ;",
    (1, 2): 'scanf("d", &kind) != EOF) {',
    (2, 3): 'kind != EOF',
    (2, 31): 'kind == EOF ',
    (3, 4): "kind == 0",
    (3, 13): "kind == 1",
    (3, 20): "kind == 2",
    (3, 26): "default",
    (4, 5): "nop",
    (5, 6): "top >= SIZE",
    (5, 8): "top < SIZE",
    (6, 7): 'fprintf(stderr, "fatal error stack overflow");',
    (7, 31): 'exit(1)',
    (8, 9): 'fprintf(stderr, "enter data to push");',
    (9, 10): 'scanf("d", &data);',
    (10, 11): 'stack[top] = data',
    (11, 12): 'top = top + 1',
    (12, 30): 'break',
    (13, 14): 'nop',
    (14, 15): 'top <= 0',
    (14, 17): 'top > 0',
    (15, 16): 'fprintf(stderr, "fatal error stack underflow")',
    (16, 31): 'exit(2)',
    (17, 18): 'top = top - 1',
    (18, 19): 'printf("top of the stack is d", stack[top])',
    (19, 30): 'break',
    (20, 21): 'nop',
    (21, 22): 'i = 0',
    (22, 23): 'i < top',
    (22, 25): 'i >= top',
    (23, 24): 'printf("stack d =d", i, stack[i])',
    (24, 22): 'i = i + 1',
    (25, 30): 'break',
    (26, 27): 'nop',
    (27, 28): 'fprintf(stderr, "fatal error unknown operation")',
    (28, 31): 'exit(3)',
    (29, 30): 'break',
    (30, 1): 'loop',
    }  # for debugging

combiners = {    
    0: [State.join,State.join],
    1: [State.widening,State.narrowing],
    2: [State.join,State.join],
    3: [State.join,State.join],
    4: [State.join,State.join],
    5: [State.join,State.join],
    6: [State.join,State.join],
    7: [State.join,State.join],
    8: [State.join,State.join],
    9: [State.join,State.join],
    10: [State.join,State.join],
    11: [State.join,State.join],
    12: [State.join,State.join],
    13: [State.join,State.join],
    14: [State.join,State.join],
    15: [State.join,State.join],
    16: [State.join,State.join],
    17: [State.join,State.join],
    18: [State.join,State.join],
    19: [State.join,State.join],  
    20: [State.join,State.join],
    21: [State.join,State.join],
    22: [State.widening,State.narrowing],
    23: [State.join,State.join],
    24: [State.join,State.join],
    25: [State.join,State.join],
    26: [State.join,State.join],
    27: [State.join,State.join],
    28: [State.join,State.join],
    29: [State.join,State.join],
    30: [State.join,State.join],
    31: [State.join,State.join],
}
chaotic_ex(succ, 0, iota, combiners, bottom, tr, tr_txt, "a2static.png")
"""
// Initializations 
0   top = 0 ;

   // Main loop 
1,2   while (scanf("%d", &kind) != EOF) {
3	   switch(kind) {
4	   case 0: // push
5		   if ( top >= SIZE ) {
6			   fprintf(stderr, "fatal error: stack overflow\n");
7			   exit(1);
		   }
8		   fprintf(stderr, "enter data to push\n");
9		   scanf("%d", &data);
10		   stack[top] = data;
11		   top = top + 1 ;
12		   break;
13	   case 1: // pop
14		   if (  top <= 0) {
15			   fprintf(stderr, "fatal error: stack underflow\n");
16			   exit(2);
		   }
17		   top = top - 1 ;
18		   printf("top of the stack is %d\n", stack[top]) ;
19		   break;
20	   case 2: // print
21		   i = 0 ;
22		   while (i < top ) {
23			   printf("stack[%d]=%d\n", i, stack[i]);
24			   i = i + 1 ;
		   }
25		   break;

26	   default: 
27		   fprintf(stderr, "fatal error: unknown operation\n");		   
28		   exit(3);
29		   break ;
30	   }
31   }
   """